Tau is a robust and general purpose, interactive (live on the web), user-configurable automated theorem prover for first-order predicate logic with equality. Tau proves both theorems and arguments expressed in unrestricted first-order notation in the KIF (knowledge interchange format) language. It combines rule-based problem rewriting with model elimination (both full and weak), uses Brand’s modification method to implement equality handling, and accepts user-configurable heuristic search to speed the search for proofs. Tau optionally implements mathematical induction (both strong and weak). Formulas are input and output in KIF or its own infix first-order syntax, and other syntactic forms can be added. Tau is operated from a Web interface or from a command-line interface. It is implemented entirely in Java.
Other features include tautology and subsumption deletion; depth-, breadth-, and modified-best-searching; use of unit lemmas; instantiation and generalization strategies; finite model checking; extensibility.